package kb;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;

import preprocessor.Simplification;
import preprocessor.absorption.Absorption;
import preprocessor.absorption.BinaryAbsorption;
import preprocessor.absorption.BinaryAbsorptionGuarded;
import preprocessor.absorption.BinaryAbsorptionGuardedExistentials;
import preprocessor.absorption.UnaryAbsorption;
import preprocessor.absorption.EquivalenceAbsorption;
import preprocessor.absorption.RoleAbsorption;
import utils.exception.ConceptException;
import utils.exception.CoreReasoningException;
import utils.exception.SyntaxParsingException;
import entities.axiom.Axiom;
import entities.axiom.ConceptAxiom;
import entities.axiom.EquivalenceAxiom;
import entities.axiom.FeatureDomainAxiom;
import entities.axiom.InclusionAxiom;
import entities.axiom.RoleAxiom;
import entities.axiom.RoleInclusionAxiom;
import entities.axiom.RoleInverseAxiom;
import entities.axiom.RoleTransitiveAxiom;
import entities.concept.AndConcept;
import entities.concept.AtomicConcept;
import entities.concept.Concept;
import entities.concept.DomainConcept;
import entities.concept.NotConcept;
import entities.concept.OrConcept;
import entities.role.Role;

/**
 * 
 * An unfoldable TBox Tu meets to the following conditions: <br>
 * 1. of the form A=>C or A=C <br>
 * 2. Axioms are unique, i.e.,A occurs only once on the LHS of all axioms <br>
 * 3. Acyclic <br>
 * Note that it is necessary to perform absorption prior to this operation.
 * 
 * @see "DLHB"
 * @author j55wu
 * 
 */
public class TBox {
	// axioms contains all the original axioms without any absorption ==>
	// replaced by Tg alone
	// private HashMap<Concept,Concept> axioms = new HashMap<Concept,Concept>();
	// Tu contains axioms from absorption
	private Map<AtomicConcept, Concept> Tu;
	// Tnu contains axioms from absorption on negated concept names
	private Map<NotConcept, Concept> Tnu;
	// Tg contains GCIs.
	private Map<Concept, Concept> Tg;
	// Te contains eq axioms
	private Map<Concept, Concept> Te;
	// Tb only contains binary axioms from absorption.
	private Map<HashSet<AtomicConcept>, Concept> Tb;

	// Tf is a special sub Tbox for absorbing f=* -> f=k, required in computing
	// rep concepts only.
	private Map<DomainConcept<?, ?>, Set<Concept>> Tf;

	// private int numofAX;
	private Set<ConceptAxiom> originalAxioms;
	// private static Set<DomainConcept> gciFeatures = new
	// HashSet<DomainConcept>();

	private BinaryAbsorptionGuarded specialBinary;
	private BinaryAbsorptionGuardedExistentials lessSpecialBinary;
	
	private RBox rbox;
	
	// public Set<DomainConcept> getGciFeatures() {
	// return gciFeatures;
	// }

	// private static Set<DomainConcept> axiomFeatures = new
	// HashSet<DomainConcept>();
	//
	// public Set<DomainConcept> getAxiomFeatures() {
	// return axiomFeatures;
	// }

	private boolean compiled;

	public boolean getCompiledStatus() {
		return this.compiled;
	}

	public void recordOriginalAxiom(ConceptAxiom ax) {
		this.originalAxioms.add(ax);
	}

	public Set<ConceptAxiom> getOriginalTBoxAxioms() {
		return this.originalAxioms;
	}
	
	public void setOriginalTBoxRBoxAxioms(Set<Axiom>  axs){
		this.originalAxioms.clear();
		this.rbox.clearOriginalAxioms();
		for(Axiom ax:axs){
			if(ax instanceof ConceptAxiom){
				this.recordOriginalAxiom(ax.asConceptAxiom());
			}else if(ax instanceof RoleAxiom){
				this.rbox.addOriginalAxioms(ax.asRoleAxiom());
			}
		}
	}
	
	
	public Set<Axiom> getOriginalTBoxRBoxAxioms(){
		Set<Axiom> allax = new HashSet<Axiom>();
		allax.addAll(this.originalAxioms);
		allax.addAll(this.rbox.getOriginalAxioms());
		return allax;
	}
	
	public static Set<InclusionAxiom> allAxiomsAsInclusions(Set<ConceptAxiom> ax){
		Set<InclusionAxiom> ret = new HashSet<InclusionAxiom>();
		for(ConceptAxiom x:ax){
			if(x instanceof InclusionAxiom){
				ret.add((InclusionAxiom) x);
			}else if(x instanceof EquivalenceAxiom){
				EquivalenceAxiom e = (EquivalenceAxiom) x;
				ret.add(new InclusionAxiom(e.getLHS(), e.getRHS()));
				ret.add(new InclusionAxiom(e.getRHS(), e.getLHS()));
			}else{
				System.err.println("Concept axiom not handled while converting to inclusions: "+x);
			}
		}
		return ret;
	}
	
	// (A or B)->C becomes A->C and B->C
	public static Set<InclusionAxiom> elimLeftDisjunctionAxioms(Set<InclusionAxiom> as){
		Set<InclusionAxiom> ret = new HashSet<InclusionAxiom>();
		for(InclusionAxiom ax: as){
			for(Concept lhs: Concept.reduceToDisjuncts(ax.getLHS())){
				ret.add(new InclusionAxiom(lhs, ax.getRHS()));
			}
		}
		return ret;
	}
	
	//A->B and C becomes two axioms A->B and A->C
	public static Set<InclusionAxiom> elimRightConjunctionAxioms(Set<InclusionAxiom> as){
		Set<InclusionAxiom> ret = new HashSet<InclusionAxiom>();
		for(InclusionAxiom ax: as){
			for(Concept rhs: Concept.reduceToConjuncts(ax.getRHS())){
				ret.add(new InclusionAxiom(ax.getLHS(),rhs));
			}
		}
		return ret;
	}

	public void setCompiledStatus(boolean b) {
		this.compiled = b;
		return;
	}

	public BinaryAbsorptionGuarded getSpecialBinaryClass() {
		return this.specialBinary;
	}
	
	public BinaryAbsorptionGuardedExistentials getLessSpecialBinaryClass(){
		return this.lessSpecialBinary;
	}

	public static void clearStatVars(){
		gcis = null;
	}
	public TBox() {
		clearStatVars();
		this.originalAxioms = new HashSet<ConceptAxiom>();
		Tu = new HashMap<AtomicConcept, Concept>();
		Tg = new HashMap<Concept, Concept>();
		Te = new HashMap<Concept, Concept>();
		Tf = new HashMap<DomainConcept<?, ?>, Set<Concept>>();
		specialBinary = new BinaryAbsorptionGuarded();
		lessSpecialBinary = new BinaryAbsorptionGuardedExistentials();
		this.rbox = new RBox();
		// this mapping should contain all the parsed pairs of (= f k);
		// domainMap = new HashMap<Object, Object>();
		/*
		 * for(DomainConcept dc:dcs){ this.insertDomainConcept(dc); }
		 */
//		if (Absorption.BA) {
			Tb = new HashMap<HashSet<AtomicConcept>, Concept>();
//		}
//		if (Absorption.NCA) {
			Tnu = new HashMap<NotConcept, Concept>();
//		}
		this.compiled = false;
	}
	
	public void setRBox(RBox rb){
		this.rbox = rb;
	}
	
	public void setTf(Map<DomainConcept<?, ?>, Set<Concept>> Tf){
		this.Tf = Tf;
	}

	/**
	 * If absorptions generate any GCIs, save them somewhere for further
	 * absorptions.
	 * 
	 * @see UnaryAbsorption
	 */
	public void saveGeneratedGCIs(Concept lhs, Concept rhs) {
		insertTg(lhs, rhs);
	}
	
	public RBox getRoleBox(){
		return this.rbox;
	}
	
	public void insertRoleAxiom(RoleAxiom ax,boolean addInverse) throws CoreReasoningException{
		//record original axioms as they are added
		this.rbox.addOriginalAxioms(ax);
		if(ax instanceof RoleInclusionAxiom){
			this.insertRoleIncAxiom((RoleInclusionAxiom) ax, addInverse);
		}else if(ax instanceof RoleInverseAxiom){
			insertRoleInverseAxiom((RoleInverseAxiom) ax, addInverse);
		}else if(ax instanceof FeatureDomainAxiom){
			FeatureDomainAxiom fd = (FeatureDomainAxiom) ax;
			try {
				this.rbox.addFeatureDomain(fd.getFeature(), fd.getDom());
			} catch (SyntaxParsingException e) {
				e.printStackTrace();
			}
		}else if(ax instanceof RoleTransitiveAxiom){
			RoleTransitiveAxiom tr = (RoleTransitiveAxiom) ax;
			this.rbox.insertTransRole(tr.getTransRole(), addInverse);
		}
		
		else{
			throw new CoreReasoningException("Unrecognized role axiom: "+ax);
		}
	}
	
	private void insertRoleInverseAxiom(RoleInverseAxiom ax, boolean inv){
		try {
			this.rbox.setInverseRoles(ax.getLeftRole(), ax.getRightRole());
		} catch (CoreReasoningException e) {
			e.printStackTrace();
		}
	}
	
	//insert a role inclusion into the role box, possibly with inverses.
	private void insertRoleIncAxiom(RoleInclusionAxiom ax, boolean addInverse){
		this.insertRoleIncAxiom(ax.getSubRole(), ax.getSuperRole(), addInverse);
	}
	
	private void insertRoleIncAxiom(Role rl, Role rr, boolean addInverse){
		this.rbox.insertRoleInclusionAxiom(rl, rr);
		if(addInverse){
			Role irl = this.rbox.getInverseRole(rl);
			Role irr = this.rbox.getInverseRole(rr);
			this.rbox.insertRoleInclusionAxiom(irl, irr);
		}
	}
	


	public Map<AtomicConcept, Concept> getTu() {
		return this.Tu;
	}

	public Map<DomainConcept<?, ?>, Set<Concept>> getTf() {
		return this.Tf;
	}

	public void insertTf(DomainConcept<?, ?> lhs, Concept rhs) {
		if (rhs.isTop()) {
			return;
		}
		Set<Concept> add = null;
		if (this.Tf.containsKey(lhs)) {
			add = this.Tf.get(lhs);
		} else {
			add = new HashSet<Concept>();
		}
		add.add(rhs);
		this.Tf.put(lhs, add);
	}

	public Map<NotConcept, Concept> getTnu() {
		return this.Tnu;
	}

	public Map<Concept, Concept> getTg() {
		return this.Tg;
	}
	
	
	private static Set<Concept> gcis = null;
	public Set<Concept> getTgAsSet() {
		if(gcis == null){
			 gcis = new HashSet<Concept>();
			for (Concept k : this.Tg.keySet()) {
				if (k.isTop()) {
					gcis.add(this.Tg.get(k));
				} else {
					gcis.add(new OrConcept(Simplification.NNF(
							new NotConcept(k), false), this.Tg.get(k)));
				}
			}
		}
		return gcis;
	}

	public Map<Concept, Concept> getTe() {
		return this.Te;
	}

	public Map<HashSet<AtomicConcept>, Concept> getTb() {
		return this.Tb;
	}
	
	//private 
	public void addAxioms(Set<Axiom> axs, boolean prime) 
			throws CoreReasoningException, SyntaxParsingException{
		//first add all inverses
		for(Axiom ax:axs){
			if(ax instanceof RoleInverseAxiom){
				this.insertRoleAxiom(ax.asRoleAxiom(), true);
			}
		}
		//add all other axioms now
		for(Axiom ax:axs){
			if(ax instanceof RoleInverseAxiom){
				continue;
			}
			if(ax instanceof ConceptAxiom){
				this.mapAxiom(ax.asConceptAxiom());
				this.recordOriginalAxiom(ax.asConceptAxiom());
				if (prime) {
					ax = ax.getPrimeCopy();
					this.mapAxiom(ax.asConceptAxiom());
				}
			}else if(ax instanceof RoleAxiom){
				try {
					this.insertRoleAxiom(ax.asRoleAxiom(), true);
					if (prime) {
						ax = ax.getPrimeCopy();
						this.insertRoleAxiom(ax.asRoleAxiom(), true);
					}
				} catch (CoreReasoningException e) {
					e.printStackTrace();
				}

			}else{
				throw new SyntaxParsingException("Unknown axiom found in the KB: "+ax);
			}
		}
	}

	// insert an axiom in general, only supports EQ, IMPLIES axioms
	private void mapAxiom(ConceptAxiom ax) {
		// put an axiom in the map
		if (ax instanceof InclusionAxiom) {
			this.insertTg(ax);
		} else if (ax instanceof EquivalenceAxiom) {
			this.insertTe((EquivalenceAxiom) ax);
		} else {
			System.err
					.println("Manual insertion of axioms is restricted to EQ, IMPLIES axioms, not: "
							+ ax.getClass());
		}
	}


	public void insertTe(EquivalenceAxiom ax) {
		Concept lhs = ax.getLHS();
		if (Te.keySet().contains(lhs)) {
			HashSet<Concept> cons = new HashSet<Concept>();
			cons.add(Te.get(lhs));
			cons.add(ax.getRHS());
			Te.put(lhs, new AndConcept(cons));
		} else {
			Te.put(lhs, ax.getRHS());
		}
	}

	public void insertTe(Concept lhs, Concept rhs) {
		if (Tg.keySet().contains(lhs)) {
			HashSet<Concept> cons = new HashSet<Concept>();
			cons.add(Te.get(lhs));
			cons.add(rhs);
			Te.put(lhs, new AndConcept(cons));
		} else {
			Te.put(lhs, rhs);
		}
	}

	/**
	 * A set of operations to push and get axioms for Tg, Tu, etc.
	 */
	public void insertTg(ConceptAxiom ax) {
		this.insertTg(ax.getLHS(), ax.getRHS());
	}

	public void insertTg(Concept lhs, Concept rhs) {
		if (Tg.keySet().contains(lhs)) {
			HashSet<Concept> cons = new HashSet<Concept>();
			cons.add(Tg.get(lhs));
			cons.add(rhs);
			Tg.put(lhs, new AndConcept(cons));
		} else {
			Tg.put(lhs, rhs);
		}
	}

	// public static void addToTBox(TBox tb, String fileName) throws
	// IOException{
	// Set<Axiom> axs = KBAccess.processAxiomFile(fileName);
	// if(axs.size()>0){
	// //add to Tg
	// tb.insertTg(axs);
	// }
	// tb.setCompiledStatus(false);
	// return;
	// }

	// overloading
	public void insertTg(Set<ConceptAxiom> axs) {
		for (ConceptAxiom ax : axs) {
			insertTg(ax);
		}
	}

	public void insertTu(ConceptAxiom ax) throws ConceptException {
		if (!(ax.getLHS() instanceof AtomicConcept)) {
			throw new ConceptException("Axiom " + ax.toString()
					+ " will not be unfoldable.");
		}
		AtomicConcept lhs = (AtomicConcept) ax.getLHS();
		this.insertTu(lhs, ax.getRHS());
	}

	public void insertTu(AtomicConcept plhs, Concept rhs)
			throws ConceptException {
		if (Tu.keySet().contains(plhs)) {
			HashSet<Concept> cons = new HashSet<Concept>();
			cons.add(Tu.get(plhs));
			cons.add(rhs);
			Tu.put(plhs, Concept.getConjunctiveConcept(cons));
		} else {
			Tu.put(plhs, rhs);
		}
	}
	
	public void removeFromTu(AtomicConcept plhs, Concept rhs)
			throws ConceptException {
		if (Tu.keySet().contains(plhs)) {
			Set<Concept> cons = Concept.reduceToConjuncts(Tu.get(plhs));
			if(!cons.contains(rhs)){
				return;
			}
			cons.remove(rhs);
			Concept newrhs = Concept.getConjunctiveConcept(cons);
			if(!newrhs.isTop()){
				Tu.put(plhs, newrhs);
			}else{
				Tu.remove(plhs);
			}
		} else {
			return;
		}
	}

	public void insertTu(HashSet<ConceptAxiom> axs) {
		for (ConceptAxiom ax : axs) {
			try {
				insertTu(ax);
			} catch (ConceptException e) {
				e.printStackTrace();
			}
		}
	}

	public void insertTnu(ConceptAxiom ax) throws ConceptException {
		if (!(ax.getLHS() instanceof NotConcept)) {
			throw new ConceptException("Axiom " + ax.toString()
					+ " cannot be inserted into Tnu.");
		}
		NotConcept lhs = (NotConcept) ax.getLHS();
		if (Tnu.keySet().contains(lhs)) {
			HashSet<Concept> cons = new HashSet<Concept>();
			cons.add(Tnu.get(lhs));
			cons.add(ax.getRHS());
			Tnu.put(lhs, new AndConcept(cons));
		} else {
			Tnu.put(lhs, ax.getRHS());
		}
	}

	// overoading
	public void insertTnu(NotConcept lhs, Concept rhs) throws ConceptException {
		// if(! (lhs instanceof NotConcept)){
		// throw new
		// ConceptException("LHS mismatch! Axiom cannot be inserted into Tnu.");
		// }
		if (Tnu.keySet().contains(lhs)) {
			HashSet<Concept> cons = new HashSet<Concept>();
			cons.add(Tnu.get(lhs));
			cons.add(rhs);
			Tnu.put(lhs, new AndConcept(cons));
		} else {
			Tnu.put(lhs, rhs);
		}
	}

	public void insertTnu(HashSet<ConceptAxiom> axs) {
		for (ConceptAxiom ax : axs) {
			try {
				insertTnu(ax);
			} catch (ConceptException e) {
				e.printStackTrace();
			}
		}
	}

	public void insertTb(ConceptAxiom ax) throws ConceptException {
		if (!(ax.getLHS() instanceof AndConcept)) {
			throw new ConceptException("Axiom " + ax.toString()
					+ " cannot be inserted into Tb.");
		}
		AndConcept lhs = (AndConcept) ax.getLHS();
		this.insertTb(lhs.getConceptSet(), ax.getRHS());
		return;
	}

	public void insertTb(Set<Concept> lhs, Concept rhs) throws ConceptException {
		if (lhs.size() != 2) {
			throw new ConceptException(
					"LHS must contain only 2 concept names. Cannot be inserted into Tb.");
		}
		HashSet<AtomicConcept> newlhs = new HashSet<AtomicConcept>();
		for (Concept c : lhs) {
			if (!(c instanceof AtomicConcept)) {
				throw new ConceptException("LHS not atomic:" + c);
			} else {
				newlhs.add((AtomicConcept) c);
			}
		}
		if (Tb.keySet().contains(newlhs)) {
			HashSet<Concept> cons = new HashSet<Concept>();
			cons.add(Tb.get(newlhs));
			cons.add(rhs);
			Tb.put(newlhs, new AndConcept(cons));
		} else {
			Tb.put(newlhs, rhs);
		}
		return;
	}

	public void insertTb(HashSet<ConceptAxiom> axs) {
		for (ConceptAxiom ax : axs) {
			try {
				insertTb(ax);
			} catch (ConceptException e) {
				e.printStackTrace();
			}
		}
	}

	public boolean compileTBox() {
		if (!this.compiled) {
			//first compile rbox
			this.rbox.compileRBox();
			return absorbAxioms();
		}
		return true;
	}

	/**
	 * This is the method for axiom absorption. Note that for guarded reasoning,
	 * binary axioms involving nominals are absorbed directly, not via this
	 * method.
	 * 
	 * @see Convertion class
	 */
	private boolean absorbAxioms() {
		boolean suc = false;
		// break equivalences
		if (Absorption.EQA || this.Te.size() > 0) {
			EquivalenceAbsorption ea = new EquivalenceAbsorption(this);
			ea.absorb();
		}
		if (this.Tg.size() < 1) {
			return true;
		}
		if (Absorption.CA || Absorption.NCA || Absorption.ECA) {
			UnaryAbsorption ca = new UnaryAbsorption(this,
					UnaryAbsorption.CA_ORDER.CA_FIRST);
			suc &= ca.absorb();
		}
		if (Absorption.BA && !Absorption.BA_Limited) {
			BinaryAbsorption ba = new BinaryAbsorption(this);
			suc &= ba.absorb();
		}
		if (Absorption.RA) {
			RoleAbsorption ra = new RoleAbsorption(this);
			suc &= ra.absorb();
		}
		this.compiled = true;
		// if(!Completion.featureGuardsInRule){
		// //if feature are to be added in axioms, get feature guards as well
		//
		// }
		// this.findFeaturesInAxioms();
		return suc;
	}

	// find all features occurring in axioms
	// Note that if f=k occurs in a GCI and in an absorbed axiom
	// GCI has the priority to deposit DEFf everywhere
	// i.e., DEFf has the dependency set {}.
	// private void findFeaturesInAxioms(){
	// if(Absorption.CA && this.Tu.size()>0){
	// for(Concept c:this.Tu.values()){
	// axiomFeatures.addAll(this.findDomainConcept(c));
	// }
	// }
	// if(Absorption.NCA && this.Tnu.size()>0){
	// for(Concept c:this.Tnu.values()){
	// axiomFeatures.addAll(this.findDomainConcept(c));
	// }
	// }
	// if(Absorption.BA && this.Tb.size()>0){
	// for(Concept c:this.Tb.values()){
	// axiomFeatures.addAll(this.findDomainConcept(c));
	// }
	// }
	// }

	// private Set<DomainConcept<?,?>> findDomainConcept(Concept c){
	// Set<DomainConcept<?,?>> ret = new HashSet<DomainConcept<?,?>>();
	// if(c instanceof AtomicConcept){
	// return ret;
	// }else if(c instanceof AndConcept){
	// AndConcept ac = (AndConcept) c;
	// for(Concept cp : ac.getConceptSet()){
	// ret.addAll(findDomainConcept(cp));
	// }
	// }else if(c instanceof OrConcept){
	// OrConcept ac = (OrConcept) c;
	// for(Concept cp : ac.getConceptSet()){
	// ret.addAll(findDomainConcept(cp));
	// }
	// }else if(c instanceof DomainConcept){
	// ret.add((DomainConcept<?, ?>) c);
	// }else if(c instanceof ExistsConcept){
	// ret.addAll(findDomainConcept(((ExistsConcept)c).getFiller()));
	// }else if(c instanceof UniversalConcept){
	// ret.addAll(findDomainConcept(((UniversalConcept)c).getFiller()));
	// }else if(c instanceof NotConcept){
	// //important: must be in NNF such that ~ does not apply to domain
	// concepts!
	// ret.addAll(findDomainConcept(((NotConcept)c).getConcept()));
	// }
	// return ret;
	// }

	/*
	 * public boolean testDomainConcept(Object f, Object k){
	 * if(this.domainMap.containsKey(f)){ if(!k.equals(this.domainMap.get(f))){
	 * return false; } } return true; }
	 */

	/*
	 * public boolean insertDomainConcept(Object f, Object k){ boolean
	 * insert=true; if(f instanceof Role && k instanceof Role){ //replacement of
	 * forks??? }else{ Role r = (f instanceof Role)? (Role) f: (Role) k; Object
	 * v = (f instanceof Role)? k: f; if(!this.domainMap.containsKey(r)){ //no
	 * such entry this.domainMap.put(r, v); }else if(!this.testDomainConcept(r,
	 * v)){ //a clash! insert = false; } } return insert; }
	 */

	/*
	 * public boolean insertDomainConcept(DomainConcept dc){ return
	 * this.insertDomainConcept(dc.getFeature(), dc.getValue()); }
	 */

	/*
	 * public HashMap<Object, Object> getDomainMap(){ return this.domainMap; }
	 */

	@Override
	public String toString() {
//		String ret = "";
//		ret += "\n=============\nAxioms in the TBox " + Display.TBOXUNICODE
//				+ ":\n=============\n";
//		Map<?, ?> maps[] = { Tu, Tnu, Tg, Tb };
//		String[] names = { "Unary Axioms", "Unary Axioms (Negated)",
//				"General Axioms (GCI)", "Binary Axioms", "DEFINITIONS" };
//		for (int i = 0; i < maps.length; i++) {
//			Map<?, ?> map = maps[i];
//			ret += "---------" + names[i] + "---------\n";
//			if (map == null || map.size() < 1) {
//				continue;
//			}
//			for (Entry<?, ?> e : map.entrySet()) {
//				ret += (i == 2 ? "[GCI] " : "") + e.getKey().toString()
//						+ " => " + e.getValue() + "\n";
//			}
//		}
//		ret += "---------" + names[names.length - 1] + "---------\n";
//		for (Entry<?, ?> e : Te.entrySet()) {
//			ret += e.getKey().toString() + " *=* " + e.getValue() + "\n";
//		}
//		//role box
//		ret += this.rbox.toString();
//		return ret;
		StringBuilder sb = new StringBuilder();
		sb = this.save(sb);
		return sb.toString();
		
	}

	public StringBuilder save(StringBuilder sb) {
		sb.append("######### Axioms in the TBox ###########\n");
		sb.append("######### Unary axioms ###########\n");
		for (Concept lhs : Tu.keySet()) {
			sb.append("(implies ");
			sb.append(lhs.toSerializedString());
			sb.append(" ");
			sb.append(Tu.get(lhs).toSerializedString() + ")\n");
		}
		sb.append("######### Negative unary axioms ###########\n");
		for (Concept lhs : Tnu.keySet()) {
			sb.append("(implies ");
			sb.append(lhs.toSerializedString());
			sb.append(" ");
			sb.append(Tnu.get(lhs).toSerializedString() + ")\n");
		}
		sb.append("######### GCIs ###########\n");
		for (Concept lhs : Tg.keySet()) {
			sb.append("(implies ");
			sb.append(lhs.toSerializedString());
			sb.append(" ");
			sb.append(Tg.get(lhs).toSerializedString() + ")\n");
		}
		sb.append("######### Definitional axioms ###########\n");
		for (Concept lhs : Te.keySet()) {
			sb.append("(equals ");
			sb.append(lhs.toSerializedString());
			sb.append(" ");
			sb.append(Te.get(lhs).toSerializedString() + ")\n");
		}
		sb.append("######### Binary axioms ###########\n");
		for (HashSet<AtomicConcept> bs : Tb.keySet()) {
			sb.append("(implies (and ");
			for (Concept b : bs) {
				sb.append(b.toSerializedString());
				sb.append(" ");
			}
			sb.append(") ");
			sb.append(" ");
			sb.append(Tb.get(bs).toSerializedString() + ")\n");
		}
		// limited binary entries?
		Map<AtomicConcept, Map<AtomicConcept, Concept>> limit = this.specialBinary
				.getTbLimited();
		this.saveBinaryAxioms(limit, sb);
		limit = this.lessSpecialBinary.getTbLimited();
		this.saveBinaryAxioms(limit, sb);
		//save rbox
		this.rbox.save(sb);
		// end
		return sb;
	}
	
	private void saveBinaryAxioms(Map<AtomicConcept, Map<AtomicConcept, Concept>> limit, 
			StringBuilder sb){
		for (AtomicConcept o : limit.keySet()) {
			Map<AtomicConcept, Concept> ds = limit.get(o);
			for (AtomicConcept d : ds.keySet()) {
				sb.append("(implies (and ");
				sb.append(o.toSerializedString());
				sb.append(" ");
				sb.append(d.toSerializedString());
				sb.append(") ");
				sb.append(ds.get(d).toSerializedString());
				sb.append(")\n");
			}
		}
	}

}
